$\forall$${\it es}$:ES, $A$:Type, $X$:AbsInterface($A$). es{-}interface{-}empty(${\it es}$;$X$) $\in$ $\mathbb{P}$